`:top
`!Spec#`! ist eine von `F33f`_`[Microsoft Research`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Microsoft_Research]`_`f entwickelte `F33f`_`[objektorientierte Programmiersprache`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Objektorientierte_Programmierung]`_`f, die eine Erweiterung zum etablierten `F33f`_`[C#`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=C-Sharp]`_`f ist`:cite-ref-1[`F5bf`_`[1`#cite-note-1]`_`f]. Sie ist kostenlos und u. a. für die `F33f`_`[Entwicklungsumgebungen`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Integrierte_Entwicklungsumgebung]`_`f `F33f`_`[Microsoft Visual Studio`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Microsoft_Visual_Studio]`_`f 2003, 2005 und 2008 verfügbar und bildet zusätzlich den Grundstock für `F33f`_`[Sing#`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Sing-Sharp]`_`f. Diese Sprache wurde für das Projekt `F33f`_`[Singularity`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Singularity_(Microsoft)]`_`f entwickelt. Die Konzepte sind zum Teil als Code Contracts in Visual Studio 2010 eingeflossen.
>>Contents
• `F0af`_`[Konzept`#konzept]`_`f
• `F0af`_`[Programmierbeispiel`#programmierbeispiel]`_`f
• `F0af`_`[Siehe auch`#siehe-auch]`_`f
• `F0af`_`[Weblinks`#weblinks]`_`f
• `F0af`_`[Einzelnachweise`#einzelnachweise]`_`f
-─
>>Konzept
Spec# ist eine Erweiterung von C# um Vorbedingungen, Nachbedingungen, Non-Null-Types und Objektinvarianzen. Die Methodenbedingungen werden durch Kontrakte abgebildet und erweitern damit die Metabeschreibung eines Objekts. Zusätzlich werden `F33f`_`[Checked Exceptions`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Ausnahmebehandlung]`_`f implementiert. Die Erweiterungen sind durch den Spec#-Compiler möglich. Für die Absicherung wurde ein `F33f`_`[Theorembeweiser`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Maschinengestütztes_Beweisen]`_`f mit dem Codenamen Boogie implementiert.
>>Programmierbeispiel
Die folgenden Zeilen geben einen kleinen Einblick in den Aufbau und die Verwendung von Spec#. Hierbei handelt es sich um den Start-`F33f`_`[Quelltext`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Quelltext]`_`f, der von Visual Studio 2005 über den Projekt-`F33f`_`[Wizard`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Assistent_(Datenverarbeitung)]`_`f für eine `F33f`_`[Konsolenanwendung`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Konsolenanwendung]`_`f generiert wird:
`B100`F9d9using System;`f`b
`B100`F9d9`f`b
`B100`F9d9public class Program`f`b
`B100`F9d9{`f`b
`B100`F9d9 static void Main(string![]! args)`f`b
`B100`F9d9`f`b
`B100`F9d9 // The following precondition is redundant with the type`f`b
`B100`F9d9 // signature for the parameter, but shown here as an example.`f`b
`B100`F9d9 requires forall{int i in (0:args.Length); args[i] != null};`f`b
`B100`F9d9 {`f`b
`B100`F9d9 Console.WriteLine("Spec# says hello!");`f`b
`B100`F9d9 }`f`b
`B100`F9d9}`f`b
>>Siehe auch
• `F33f`_`[Eiffel (Programmiersprache)`:/page/entry.mu`zim=wikipedia_de_all_nopic_2026-01.zim|entry_path=Eiffel_(Programmiersprache)]`_`f
>>Weblinks
• Offizielle Webseite (englisch)
• Expert to Expert: Contract Oriented Programming and Spec# (Erik Meijer im Gespräch mit den Spec#-Designern auf Channel9) (englisch)
• Code Contracts in .NET 4 (englisch)
>>Einzelnachweise
`:cite-note-1`!1.`! `F0af`_`[↑`#cite-ref-1]`_`f `*Spec#.`* In: `*Microsoft Research.`* Abgerufen am 16. Dezember 2018 (amerikanisches Englisch).
`c`F0af`_`[↑ Back to top`#top]`_`f`a